/* =============================================================================
 * PROJET           	: Matrices creuses
 * NOM DU FICHIER   	: Traitement.c
 * OBJET            	: Paquetage contenant les fonctions de traitement
 * -----------------------------------------------------------------------------
 * DATE DE CREATION 	: 10/04/2009
 * AUTEUR           	: Ivan VALIMAHAMED, Sha LIU, Yves BOGE
 * -----------------------------------------------------------------------------
 * MODIFICATIONS (   n) date - auteur - description )
 * ============================================================================= */

#include "Traitement.h"

/* Taille maximum que peut prendre la chaine de caracteres de la fonction : */
#define TAILLE_MAX_FCT 100000

/* Taille maximum que peut prendre la chaine de caracteres de la fonction : */
#define NB_MAX_VAR 1000


/*
 *	NOM 				: Choisir_valeur
 *	ENTREES 			: i_No_var numero de la variable choisie
 *						: io_Mat matrice de type t_Matrice
 *	SORTIES			: valeur choisie pour la variable Xi (0 ou 1)
 *	BUT				: recherche une valeur possible a affecter a Xi
 */

int Choisir_valeur(int i_No_var, t_Matrice* io_Mat)
{
	int V = 2;

	if ( io_Mat->Var[i_No_var - 1].Premier != NULL )
	{
		if ( io_Mat->Var[i_No_var - 1].Premier->X.Signe == true )
			V = 1;
		else
			V = 0;
	}
	return V;
}


/*
 *	NOM 				: Simplifier
 *	ENTREES 			: i numero de la variable choisie
 *						: v valeur choisie pour Xi
 *						: io_Mat matrice de type t_Matrice
 *	SORTIES			: valeur choisie pour la variable Xi (0 ou 1)
 *	BUT				: Simplifier les clauses contenant la variable Xi precedement choisie
 */

void Simplifier (int i, int v, t_Matrice* io_Mat)
{
	t_Elem* ptr_Elem;
	
	io_Mat->Var[i - 1].Valeur = v;
	
	ptr_Elem = io_Mat->Var[i - 1].Premier;

	while ( ptr_Elem != NULL )
	{
	 	/* Selon la valeur precedente du litteral, on decrementera le nb
	 	 * de litteral falsifie, neutre, ou satisfait
	 	 */
	 	if ( ptr_Elem->X.Val == 2 )
			io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_neutres--;
	 	if ( ptr_Elem->X.Val == 1 )
			io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_satisfaits--;
	 	if ( ptr_Elem->X.Val == 0 )
			io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_falsifies--;
	 		
	 	
		if ( v == 1 )
		{
			/*
			 * Si la valeur de la variable est egale a 1 alors
			 * les clauses contenant Xi sont satisfaites
			 * les clauses contenant /Xi sont raccourcies (ou eventuellement falsifiees)
			 * les clauses ne contenant ni Xi ni /Xi restent inchangees
			 */
			 if ( ptr_Elem->X.Signe == true )
			 {			 		
			 	ptr_Elem->X.Val = 1; 				/* Le litteral est satisfait*/
			 	/* Le nombre de litteraux satisfaits de la clause est incremente,
			 	 * et la clause devient satisfaite
			 	 */
			 	io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_satisfaits += 1;
			 	io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 1;
			 }
			 else /* Le litteral a pour signe '-', donc il est falsifie*/
			 {
			 	ptr_Elem->X.Val = 0;
			 	
			 	/* Le nombre de litteraux falsifie de la clause est incremente */
			 	io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_falsifies += 1;
			 	
			 	/* La clause contenant /Xi est raccourcie si aucun de ses litteraux n'est satisfait */
			 	if ( io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_satisfaits == 0 )
			 	{
			 		io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 3;
			 		
				 	/* Si /Xi etait le seul litteral alors la clause est falsifiee */
				 	if ( io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_neutres == 0 )
				 		io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 0;
			 	}
			 }
		}
		if ( v == 0 )
		{
			/*
			 * Si la valeur de la variable est egale a 0 alors
			 * les clauses contenant /Xi sont satisfaites
			 * les clauses contenant Xi sont raccourcies, falsifiees, ou éventuellement inchangés
			 * les clauses ne contenant ni Xi ni /Xi restent inchangees
			 */
			 if ( ptr_Elem->X.Signe == false )
			 {
			 	ptr_Elem->X.Val = 1; 				/* Le litteral est satisfait*/
			 	/* Le nombre de litteraux satisfaits de la clause est incremente, 
			 	 * et la clause devient satisfaite
			 	 */
			 	io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_satisfaits += 1;
			 	io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 1;
			 }
			 else /* Le litteral a pour signe '+', donc il est falsifie*/
			 {
			 	ptr_Elem->X.Val = 0;
			 	
			 	/* Le nombre de litteraux falsifie de la clause est incremente */
			 	io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_falsifies += 1;
			 			 	
			 	/* La clause contenant /Xi est raccourcie si aucun de ses litteraux n'est satisfait */
			 	if ( io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_satisfaits == 0 )
			 	{
			 		io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 3;
			 		
				 	/* Si /Xi etait le seul litteral alors la clause est falsifiee */
				 	if ( io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_neutres == 0 )
				 		io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 0;
			 	}
			 }
		}
		if ( v == 2 ) /* Reinitialisation de la matrice avec la variable a neutre*/
		{
			io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_neutres++;
			ptr_Elem->X.Val = 2;
			
			/* On met a jour l'etat de la clause */
			if ( io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_satisfaits == 0 )	/* Clause non satisfaite */
			{
				if ( io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Nb_falsifies == 0 )	/* tous les litteraux sont neutres : inchange */
					io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 2;
				else								/* Clause raccourcie */
					io_Mat->Clause[(ptr_Elem->X.Num_clause) - 1].Etat = 3;
			}
			/* Si la clause est satisfaite apres avoir passe le litteral a neutre, alors elle l'etait deja avant.
			 * On a donc rien a faire.
			 */
		}
		ptr_Elem = (t_Elem*) ptr_Elem->Clause_suiv;
	}
}



/*
 *	NOM 			: Choix_variable
 *	ENTREES 		: pointeur sur la matrice
 *	SORTIES		: o_Var : le numero de la variable choisit
 *					: o_Clause : Le numero de la clause ayant servit au choix de la variable
 *	BUT			: Choisir la variable a laquelle on va donner une valeur pour
 *					: simplifier la matrice
 */

void Choix_variable (t_Matrice* i_Matrice, int* o_Clause, int* o_Var)
{
	bool Trouve_min = false;
	int Nb_neutres_min = NB_MAX_VAR;
	int i = 0;
	t_Elem* Courant;

	/* On cherche la clause non satisfaite contenant le minimum de variables neutres */
	*o_Clause = 1;
	while ( (i < i_Matrice->Nb_clauses) && ! Trouve_min )
	{
		/* si la clause n'est pas satisfaite */
		if ( i_Matrice->Clause[i].Etat != 1 )
		{
			if ( i_Matrice->Clause[i].Nb_neutres < Nb_neutres_min )
			{
				Nb_neutres_min = i_Matrice->Clause[i].Nb_neutres;
				*o_Clause = i + 1;
			}
			/* Si le nombre de variables neutre est 1, alors on ne peut pas trouver
				mieux, donc on s'arrete de chercher */
			if ( Nb_neutres_min == 1 )
				Trouve_min = true;
		}
		i++;
	}

	/* on prend la variable du premier litteral neutre pour cette clause */
	Courant = i_Matrice->Clause[*o_Clause - 1].Premier;
	while ( Courant->X.Val != 2 )
		Courant = (t_Elem*) Courant->Var_suiv;

	*o_Var = Courant->X.Num_var;
}


/*
 *	NOM 			: Toutes_clauses_satisfaites
 *	ENTREES 		: pointeur sur la matrice
 *	SORTIES		: booleen : vrai si toutes les clauses dans la matrice sont satisfaites, faux sinon
 *	BUT			: savoir si la valeur choisit pour la variable est correcte
 */

int Toutes_clauses_satisfaites (t_Matrice* i_Matrice)
{
	int i = 0;

	/* On parcours l'ensemble des clauses */
	while ( (i < i_Matrice->Nb_clauses) && (i_Matrice->Clause[i].Etat == 1) )
		i++;

	return (i == i_Matrice->Nb_clauses);
}


/*
 *	NOM 			: Une_clause_falsifiee
 *	ENTREES 		: pointeur sur la matrice
 *	SORTIES		: booleen : vrai si la matrice a au moins une clause falsifiee, faux sinon
 *	BUT			: savoir si la valeur choisit pour la variable est correct
 */

int Une_clause_falsifiee (t_Matrice* i_Matrice)
{
	int i = 0;

	/* On parcours l'ensemble des clauses */
	while ( (i < i_Matrice->Nb_clauses) && (i_Matrice->Clause[i].Etat != 0) )
		i++;

	return (i != i_Matrice->Nb_clauses);
}



/*
 *	NOM 			: Put_fonction_reduite
 *	ENTREES 		: pointeur sur la matrice
 *	SORTIES		: void
 *	BUT			: affiche en console la fonction simplifiee
 */

void Put_fonction_reduite (t_Matrice* i_Matrice)
{
	char Chaine[TAILLE_MAX_FCT] = "";		/* chaine de caractere utilise pour le stockage de la fonction */
	int i_clause;									/* indice de parcours du tableau des clauses */
	int i_fct;										/* indice de parcours de la chaine de caractere de la fonction*/
	t_Elem* ptr_Elem;
	char String_num_var[6] = "";				/* Chaine de caracteres permettant de stocker le numero de la variable*/
	int i_num_var;									/* indice de parcours de la chaine de caractere du numero de variable*/

	/*
	 * Parcours de la matrice:
	 * On va parcourir chaque clause de la matrice:
	 * 	- Si la clause est satisfaite, alors de rien faire
	 *		- Sinon on affiche les litteraux sont neutres
	 * nous allons utiliser cette typographie:
	 * "f={{clause1},{clause2},...,{clauseN}}"
	 * les litteraux negatifs seront representes sous la forme "/x1"
	 */
	Chaine[0] = 'f'; Chaine[1] = '='; Chaine[2] = '{';
	i_fct = 3;
	for ( i_clause = 0; i_clause < i_Matrice->Nb_clauses; i_clause++ )
	{
		/* Si la clause est satifaite, on ne fait rien*/
		if ( i_Matrice->Clause[i_clause].Etat != 1 )
		{
			Chaine[i_fct] = '{';
			i_fct++;
			/* Parcours des litteraux de la clause */
			for ( ptr_Elem = (t_Elem*) i_Matrice->Clause[i_clause].Premier; ptr_Elem != NULL; ptr_Elem = (t_Elem*) ptr_Elem->Var_suiv )
			{
				/* si le litteral est neutre alors on l'affiche */
				if ( ptr_Elem->X.Val == 2 )
				{
					/* Si le signe est negatif alors on ajoute '/' */
					if ( ptr_Elem->X.Signe == false )
					{
						Chaine[i_fct] = '/';
						i_fct++;
					}
					Chaine[i_fct] = 'x'; i_fct++;

					/* On a besoin de convertir un entier en chaine de caracteres
					 * puis, on recopie cet entier dans la fonction
					 */
					sprintf(String_num_var,"%d",ptr_Elem->X.Num_var);
					for ( i_num_var = 0; i_num_var < strlen(String_num_var); i_num_var++ )
					{
						Chaine[i_fct] = String_num_var[i_num_var];
						i_fct++;
					}
					Chaine[i_fct] = ','; i_fct++;
				}
			}
			i_fct--;
			Chaine[i_fct] = '}'; i_fct++;
			Chaine[i_fct] = ','; i_fct++;
		}
	}
	if ( Chaine[i_fct-1] != '{' )
		i_fct--;
	Chaine[i_fct]='}'; i_fct++;
	Chaine[i_fct]='\0';
	printf("%s\n",Chaine);
	if ( strcmp(Chaine,"f={}") == 0 )
		printf("La fonction a ete entierement reduite\n");
}


/*
 *	NOM 			: Resolution
 *	ENTREES 		: io_Matrice : pointeur sur la matrice
 *			 		: i_Trace : booleen indiquant au programme s'il doit activer l'affichage de la trace
 *			 		: i_Matrice : booleen indiquant au programme s'il doit activer l'affichage de la matrice
 *	SORTIES		: booleen : vrai si il existe une affectation de valeurs aux variables telle que la formule ait la valeur 1, faux sinon
 *	BUT			: savois si il existe une solution pour la formule
 */

int Resolution ( t_Matrice* io_Matrice, int i_Trace, int i_Matrice )
{
   t_Litteral X;
   bool Resolu;
   
   
   if ( (bool) i_Matrice )
			Aff_matrice(io_Matrice);
   
   if ( Toutes_clauses_satisfaites(io_Matrice) )
   {
   	if ( (bool) i_Trace )
			printf("toutes les clauses sont satisfaites(on remonte)\n");
   	return (int) true;
   }
   if ( Une_clause_falsifiee(io_Matrice) )
  	{
   	if ( (bool) i_Trace )
			printf("il existe une clause falsifie (on remonte dans la recursivite)\n");
		return (int) false;
	}
		
   Choix_variable(io_Matrice, &X.Num_clause, &X.Num_var);
   X.Val = Choisir_valeur(X.Num_var, io_Matrice);
   
   if ( (bool) i_Trace )
		printf("on simplifie en mettant X%d a %d\n", X.Num_var, X.Val);
   Simplifier(X.Num_var, X.Val, io_Matrice);
   
   if ( Resolution(io_Matrice, i_Trace, i_Matrice) )
   	return (int) true;
   else
   {
      X.Val = 1 - X.Val;
      Simplifier(X.Num_var, X.Val, io_Matrice);
   	if ( (bool) i_Trace )
			printf("on modifie la valeur de la variable X%d (a %d) et on poursuit\n", X.Num_var, X.Val);
      
      Resolu = Resolution(io_Matrice, i_Trace, i_Matrice);
      if ( !Resolu )
      	Simplifier(X.Num_var, 2, io_Matrice);
      
      return Resolu;
 	}
}


/*
 *	NOM 			: Put_infos_matrice
 *	ENTREES 		: pointeur sur la matrice
 *	SORTIES		: void
 *	BUT			: affiche en console les informations permettant de visualiser
 * 				: l'etat de la matrice
 */

void Put_infos_matrice (t_Matrice* i_Matrice)
{
	/* Compteurs de variables a 0, 1 et à "neutre"*/
	int Nb_var_0 = 0;
	int Nb_var_1 = 0;
	int Nb_var_2 = 0;
	
	/* Compteurs de clauses satisfaites, falsifiees, inchangees et raccourcies */
	int Nb_clauses_satisfaites = 0;
	int Nb_clauses_falsifiees = 0;
	int Nb_clauses_inchangees = 0;
	int Nb_clauses_raccourcies = 0;
	
	int i;
	
	for ( i = 0; i< i_Matrice->Nb_var; i++ )
	{
		if ( i_Matrice->Var[i].Valeur == 0 )
			Nb_var_0++;
		if ( i_Matrice->Var[i].Valeur == 1 )
			Nb_var_1++;
		if ( i_Matrice->Var[i].Valeur == 2 )
			Nb_var_2++;
	}
	for ( i = 0; i< i_Matrice->Nb_clauses; i++ )
	{
		if ( i_Matrice->Clause[i].Etat == 0 )
			Nb_clauses_falsifiees++;
		if ( i_Matrice->Clause[i].Etat == 1 )
			Nb_clauses_satisfaites++;
		if ( i_Matrice->Clause[i].Etat == 2 )
			Nb_clauses_inchangees++;
		if ( i_Matrice->Clause[i].Etat == 3 )
			Nb_clauses_raccourcies++;
	}
	
	printf("-------------------------------------------------------------------------------\n");
	printf("                       INFORMATIONS SYNTHETIQUES                            	\n");
	printf("-------------------------------------------------------------------------------\n");
	printf("  Variables              à 0            : %d							\n", Nb_var_0);
	printf("                         à 1            : %d							\n", Nb_var_1);
	printf("                         à 2            : %d							\n", Nb_var_2);
	printf("                         TOTAL          : %d                    \n", i_Matrice->Nb_var);
	printf("-------------------------------------------------------------------------------\n");
	printf("  Clauses              satisfaites      : %d							\n", Nb_clauses_satisfaites);
	printf("                       falsifiees       : %d							\n", Nb_clauses_falsifiees);
	printf("                       inchangees       : %d							\n", Nb_clauses_inchangees);
	printf("                       raccourcies      : %d                    \n", Nb_clauses_raccourcies);
	printf("                       TOTAL            : %d                    \n", i_Matrice->Nb_clauses);
	printf("-------------------------------------------------------------------------------\n");	
}


